/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BDR30/FONT#2=BASI30/FONT#3=BASB30/FONT#4=BDR30/FONT#5=SUB/FONT#6=SUP/FONT#9=FIX40/FONT#10=FIX30
␈↓ ↓H␈↓␈↓ ε`␈↓ i1


␈↓ ↓H␈↓β␈↓ ¬⎇CHAPTER IV

␈↓ ↓H␈↓β␈↓ ¬ZCOMPUTABILITY






␈↓ ↓H␈↓1.

␈↓ ↓H␈↓1

␈↓ ↓H␈↓2␈↓βThe function ␈↓αeval␈↓.


␈↓ ↓H␈↓        Except␈αfor␈αspeed␈αand␈αmemory␈αsize␈αall␈αpresent␈αday␈αstored␈αprogram␈αcomputers␈αare␈αequivalent␈αin
␈↓ ↓H␈↓what␈α∞computations␈α∞they␈α∞can␈α∞do.␈α
 A␈α∞program␈α∞written␈α∞for␈α∞one␈α
computer␈α∞can␈α∞be␈α∞translated␈α∞to␈α∞run␈α
on
␈↓ ↓H␈↓another.␈α⊃ Indeed,␈α⊃one␈α⊃can␈α⊃write␈α⊃a␈α⊃simulator␈α⊃for␈α⊂one␈α⊃computer␈α⊃to␈α⊃run␈α⊃on␈α⊃another.␈α⊃ To␈α⊃put␈α⊃it␈α⊂in
␈↓ ↓H␈↓commercial␈α⊃terms,␈α⊃no␈α⊃computer␈α⊃manufacturer␈α⊃can␈α⊃advertise␈α⊃that␈α⊃his␈α⊃machine␈α⊃can␈α⊃do␈α⊂calculations
␈↓ ↓H␈↓impossible on the machine made by his competitors.

␈↓ ↓H␈↓        This␈αis␈αwell␈αknown␈αintuitively,␈αand␈αthe␈αfirst␈αmathematical␈αtheorem␈αof␈αthis␈αkind␈αwas␈αproved␈αby
␈↓ ↓H␈↓A.M.␈α
Turing␈α∞(1936),␈α
who␈α
defined␈α∞a␈α
primitive␈α
kind␈α∞of␈α
computer␈α
now␈α∞called␈α
a␈α
Turing␈α∞machine,␈α
and
␈↓ ↓H␈↓showed␈α⊃how␈α⊃to␈α⊃make␈α⊃a␈α⊃universal␈α⊃machine␈α⊃that␈α⊃could␈α⊃do␈α⊃any␈α⊃computation␈α⊃done␈α⊃by␈α∩any␈α⊃Turing
␈↓ ↓H␈↓machine␈α∩when␈α∩given␈α∩a␈α∩description␈α∩of␈α∩the␈α∩machine␈α∩to␈α∩be␈α∩simulated␈α∩and␈α∩the␈α∩initial␈α∩tape␈α∩of␈α∩the
␈↓ ↓H␈↓computation to be imitated.

␈↓ ↓H␈↓        In␈αLISP␈αthe␈αfunction␈α␈↓αeval␈↓␈αis␈αa␈αuniversal␈αLISP␈αfunction␈αin␈αthe␈αsense␈αthat␈αany␈αcomputation␈αdone
␈↓ ↓H␈↓by any LISP function can be done by ␈↓αeval␈↓ when ␈↓αeval␈↓ is given suitable arguments.

␈↓ ↓H␈↓        ␈↓αeval␈↓␈α∞has␈α∞two␈α
arguments␈α∞the␈α∞first␈α
of␈α∞which␈α∞is␈α∞a␈α
LISP␈α∞expression␈α∞in␈α
the␈α∞notation␈α∞given␈α∞in␈α
the
␈↓ ↓H␈↓previous␈αsection,␈α
while␈αthe␈α
second␈αis␈αa␈α
list␈αof␈α
pairs␈αthat␈α
give␈αthe␈αvalues␈α
of␈αany␈α
free␈αvariables␈αthat␈α
may
␈↓ ↓H␈↓occur␈αin␈α
the␈αexpression.␈α Since␈α
any␈αcomputation␈αcan␈α
be␈αdescribed␈αas␈α
evaluating␈αan␈αexpression␈α
without
␈↓ ↓H␈↓free␈α
variables,␈αthe␈α
second␈αargument␈α
plays␈α
a␈αrole␈α
mainly␈αin␈α
the␈α
recursive␈αdefinition␈α
of␈α␈↓αeval␈↓,␈α
and␈αwe␈α
can
␈↓ ↓H␈↓start our computations with the second argument NIL.

␈↓ ↓H␈↓        To␈α
illustrate␈α
this,␈α
suppose␈α
we␈α
want␈α
to␈α
apply␈α
the␈α
function␈α
␈↓αalt␈↓␈α
to␈α
the␈α
list␈α
(A␈α
B␈α
C␈α
D␈α
E),␈α
i.e.␈α
we␈α
wish
␈↓ ↓H␈↓to evaluate ␈↓αalt␈↓↓[␈↓∧(A B C D E)␈↓↓]␈↓.  This can be obtained by computing

␈↓ ↓H␈↓        ␈↓αeval␈↓↓[␈↓∧((LABEL ALT (LAMBDA (X) (COND ((OR (NULL X) (NULL (CDR X))) X)
␈↓ ↓H␈↓∧(T (CONS (CAR X) (ALT (CDDR X))))))) (QUOTE (A B C D E)), NIL␈↓↓]␈↓,

␈↓ ↓H␈↓and␈α∞gives␈α∞the␈α∞expected␈α∂result␈α∞(A␈α∞C␈α∞E).␈α∂ The␈α∞second␈α∞argument␈α∞of␈α∞␈↓αeval␈↓,␈α∂taken␈α∞as␈α∞NIL␈α∞in␈α∂the␈α∞above
␈↓ ↓H␈↓example␈α⊂is␈α⊂a␈α⊂list␈α⊂of␈α⊂dotted␈α⊂pairs␈α⊂where␈α⊂the␈α⊂first␈α⊂element␈α⊂of␈α⊂each␈α⊂pair␈α⊂is␈α⊂an␈α⊂atom␈α⊂representing␈α⊂a
␈↓ ↓H␈↓␈↓ ¬{CHAPTER IV␈↓ i2


␈↓ ↓H␈↓variable␈α
and␈αthe␈α
second␈αelement␈α
is␈αthe␈α
value␈α
assigned␈αto␈α
that␈αvariable.␈α
 A␈αvariable␈α
may␈α
occur␈αmore
␈↓ ↓H␈↓than␈α
once␈α
in␈α
the␈αlist␈α
and␈α
the␈α
value␈α
chosen␈αis␈α
that␈α
paired␈α
with␈α
the␈αfirst␈α
occurrence␈α
of␈α
the␈αvariable.␈α
 We
␈↓ ↓H␈↓illustrate this by the equation

␈↓ ↓H␈↓        ␈↓αeval␈↓↓[␈↓∧(CAR X), ((X.(B.C)) (Y.A) (X.B))␈↓↓] = ␈↓∧B␈↓,

␈↓ ↓H␈↓i.e.␈α
we␈α
have␈α
evaluated␈α
␈↓βa␈α
␈↓αx␈↓␈α
with␈α␈↓α␈α
x␈↓↓␈α
=␈α
␈↓∧(B.C)␈↓.␈α
 The␈α
value␈α
associated␈αwith␈α
a␈α
variable␈α
in␈α
such␈α
a␈α
list␈αof␈α
pairs
␈↓ ↓H␈↓is computed by the auxiliary function ␈↓αassoc␈↓ which has the recursive definition

␈↓ ↓H␈↓        ␈↓αassoc␈↓↓[␈↓αv, a␈↓↓] ← ␈↓βif n ␈↓αa ␈↓βthen ␈↓∧NIL ␈↓βelse if aa ␈↓αa ␈↓β eq ␈↓αv ␈↓βthen a ␈↓αa ␈↓βelse ␈↓αalt␈↓↓[␈↓αv, ␈↓βd ␈↓αa␈↓↓]␈↓.

␈↓ ↓H␈↓Thus we have ␈↓αassoc␈↓↓[␈↓∧X, ((X.(B.C)) (Y.A) (X.B))␈↓↓] = ␈↓∧(X.(B.C))␈↓.

␈↓ ↓H␈↓        A simplified version of the usual LISP ␈↓αeval␈↓ is the following:

␈↓ ↓H␈↓␈↓αeval␈↓↓[␈↓αe, a␈↓↓] ←
␈↓ ↓H␈↓↓␈↓        ␈↓↓␈↓βif at ␈↓αe ␈↓βthen ␈↓↓[␈↓βif ␈↓αnumberp e ␈↓↓∨ ␈↓αe  ␈↓βeq ␈↓∧NIL ␈↓↓∨ ␈↓αe ␈↓βeq ␈↓∧T ␈↓βthen ␈↓αe ␈↓βelse␈↓α assoc␈↓↓[␈↓αe, a␈↓↓]]
␈↓ ↓H␈↓↓␈↓        ␈↓↓␈↓βelse if at a␈↓α e ␈↓βthen
␈↓ ↓H␈↓β␈↓                ␈↓β␈↓↓[␈↓βif a ␈↓αe␈↓β eq ␈↓∧CAR ␈↓βthen a ␈↓αeval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe␈↓β eq ␈↓∧CDR ␈↓βthen d ␈↓αeval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe␈↓β eq ␈↓∧CONS ␈↓βthen ␈↓αeval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]  . ␈↓αeval␈↓↓[␈↓βadd ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe␈↓β eq ␈↓∧ATOM ␈↓βthen at ␈↓αeval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe␈↓β eq ␈↓∧EQ ␈↓βthen at ␈↓αeval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]  ␈↓βeq ␈↓αeval␈↓↓[␈↓βadd ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe␈↓β eq ␈↓∧QUOTE ␈↓βthen ad ␈↓αe
␈↓ ↓H␈↓α␈↓                ␈↓α␈↓βelse if a ␈↓αe␈↓β eq ␈↓∧COND ␈↓βthen ␈↓αevcon␈↓↓[␈↓βd ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe␈↓β eq ␈↓∧LIST ␈↓βthen ␈↓αmapcar␈↓↓[␈↓βd ␈↓αe, λx␈↓↓: ␈↓αeval␈↓↓[␈↓αx, a␈↓↓]]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse ␈↓αeval␈↓↓[␈↓βd ␈↓αassoc␈↓↓[␈↓βa ␈↓αe, a␈↓↓] . ␈↓βd ␈↓αe, a␈↓↓]]
␈↓ ↓H␈↓↓␈↓        ␈↓↓␈↓βelse if aa ␈↓αe ␈↓βeq ␈↓∧LAMBDA ␈↓βthen  ␈↓αeval␈↓↓[␈↓βadda ␈↓αe, prup␈↓↓[␈↓βada ␈↓αe, mapcar␈↓↓[␈↓βd ␈↓αe, ␈↓↓λ␈↓αx␈↓↓: ␈↓αeval␈↓↓[␈↓αx, a␈↓↓]]] * ␈↓αa␈↓↓]
␈↓ ↓H␈↓↓␈↓        ␈↓↓␈↓βelse if aa ␈↓αe ␈↓βeq ␈↓∧LABEL ␈↓βthen ␈↓αeval␈↓↓[␈↓βadda ␈↓αe . ␈↓βd ␈↓αe, ␈↓↓[␈↓βada ␈↓αe . ␈↓βa ␈↓αe␈↓↓] . ␈↓αa␈↓↓]␈↓,

␈↓ ↓H␈↓where the auxiliary function ␈↓αevcon␈↓ is defined by

␈↓ ↓H␈↓        ␈↓αevcon␈↓↓[␈↓αu, a␈↓↓] ← ␈↓βif ␈↓αeval␈↓↓[␈↓βaa ␈↓αu, a␈↓↓] ␈↓βthen ␈↓αeval␈↓↓[␈↓βada ␈↓αu, a␈↓↓]  ␈↓βelse ␈↓αevcon␈↓↓[␈↓βd ␈↓αu, a␈↓↓]␈↓,

␈↓ ↓H␈↓and␈α⊂the␈α∂auxiliary␈α⊂function␈α∂␈↓αprup␈↓␈α⊂used␈α∂for␈α⊂pairing␈α∂up␈α⊂the␈α∂elements␈α⊂of␈α∂two␈α⊂lists␈α∂of␈α⊂equal␈α⊂length␈α∂is
␈↓ ↓H␈↓defined by

␈↓ ↓H␈↓        ␈↓αprup␈↓↓[␈↓αu, v␈↓↓] ← ␈↓βif n ␈↓αu ␈↓βthen ␈↓∧NIL ␈↓βelse ␈↓↓[␈↓βa ␈↓αu  . ␈↓βa ␈↓αv␈↓↓] . ␈↓αprup␈↓↓[␈↓βd ␈↓αu, ␈↓βd ␈↓αu␈↓↓].␈↓

␈↓ ↓H␈↓        The␈α∂way␈α∂␈↓αeval␈↓␈α∂works␈α∂should␈α∂be␈α∂clear;␈α⊂atoms␈α∂are␈α∂either␈α∂immediately␈α∂evaluable␈α∂or␈α∂have␈α⊂to␈α∂be
␈↓ ↓H␈↓looked␈αup␈αon␈αthe␈αlist␈α␈↓αa␈↓;␈αexpressions␈αwhose␈αfirst␈αterm␈αis␈αone␈αof␈αthe␈αelementary␈αfunctions␈αare␈αevaluated
␈↓ ↓H␈↓by␈α⊃performing␈α⊃the␈α⊃indicated␈α⊃operation␈α⊂on␈α⊃the␈α⊃result␈α⊃of␈α⊃evaluating␈α⊂the␈α⊃arguments;␈α⊃␈↓αlist␈↓␈α⊃has␈α⊃to␈α⊂be
␈↓ ↓H␈↓handled␈αspecially,␈αbecause␈αit␈αhas␈αan␈αindefinite␈αnumber␈αof␈αarguments;␈αconditionals␈αare␈αhandled␈αby␈αan
␈↓ ↓H␈↓auxiliary␈α
function␈α
that␈α
evaluates␈α
the␈α
terms␈α
in␈αthe␈α
right␈α
order;␈α
quoted␈α
S-expressions␈α
are␈α
trivial;␈αnon-
␈↓ ↓H␈↓elementary␈α
functions␈αhave␈α
their␈α
definitions␈αlooked␈α
up␈αon␈α
␈↓αa␈↓␈α
and␈αsubstituted␈α
for␈αtheir␈α
names;␈α
when␈αa
␈↓ ↓H␈↓␈↓ ¬{CHAPTER IV␈↓ i3


␈↓ ↓H␈↓function␈α∞is␈α∞specified␈α∞by␈α∞a␈α∂λ,␈α∞the␈α∞inner␈α∞expression␈α∞is␈α∞evaluated␈α∂with␈α∞a␈α∞new␈α∞␈↓αa␈↓␈α∞which␈α∞is␈α∂obtained␈α∞by
␈↓ ↓H␈↓evaluating␈αthe␈αarguments␈α
and␈αpairing␈αthem␈α
up␈αwith␈αthe␈α
variables␈αand␈αputting␈α
them␈αon␈αthe␈α
front␈αof
␈↓ ↓H␈↓the␈αold␈α␈↓αa␈↓;␈αand␈αfinally,␈α␈↓βlabel␈↓␈αis␈αhandled␈αby␈αpairing␈αthe␈αname␈αof␈αthe␈αfunction␈αwith␈αthe␈αexpression␈αon␈α␈↓αa␈↓
␈↓ ↓H␈↓and replacing the whole function by the λ-part.

␈↓ ↓H␈↓        ␈↓αeval␈↓␈α∂plays␈α∂both␈α∞a␈α∂theoretical␈α∂and␈α∂a␈α∞practical␈α∂role␈α∂in␈α∂LISP.␈α∞ Historically,␈α∂the␈α∂list␈α∂notation␈α∞for
␈↓ ↓H␈↓LISP␈α∂functions␈α∂and␈α∂␈↓αeval␈↓␈α∂were␈α∂first␈α∂devised␈α∂in␈α∂order␈α∞to␈α∂show␈α∂how␈α∂easy␈α∂it␈α∂is␈α∂to␈α∂define␈α∂a␈α∞universal
␈↓ ↓H␈↓function␈αin␈α
LISP␈α-␈α
the␈αidea␈α
was␈αto␈αadvocate␈α
LISP␈αas␈α
an␈αalternative␈α
to␈αTuring␈α
machines␈αfor␈αdoing␈α
the
␈↓ ↓H␈↓elementary␈αtheory␈αof␈αcomputability.␈α
 The␈αnotation␈αused␈αwas␈α
chosen␈αwithout␈αmuch␈αregard␈α
for␈αhuman
␈↓ ↓H␈↓convenience,␈αbecause␈αthe␈αoriginal␈α
idea␈αwas␈αpurely␈αtheoretical;␈α
the␈αnotation␈αfor␈αconditional␈α
expressions,
␈↓ ↓H␈↓for␈α
example,␈α
has␈α
an␈α∞unnecessary␈α
extra␈α
level␈α
of␈α
parentheses.␈α∞ However,␈α
S.␈α
R.␈α
Russell␈α
noted␈α∞that␈α
␈↓αeval␈↓
␈↓ ↓H␈↓could␈αserve␈αas␈αan␈αinterpreter␈αfor␈αLISP␈α
and␈αpromptly␈αprogrammed␈αit␈αin␈αmachine␈αlanguage␈αwith␈α
minor
␈↓ ↓H␈↓modifications␈α∂for␈α∂practical␈α∂purposes.␈α∂ Since␈α∂a␈α∂compiler␈α∂was␈α∂long␈α∂delayed,␈α∂the␈α∂interpreter␈α∂was␈α∞more
␈↓ ↓H␈↓easily␈α⊂modified␈α⊂and␈α⊂handled␈α⊂some␈α⊃difficult␈α⊂cases␈α⊂with␈α⊂functional␈α⊂arguments␈α⊂better,␈α⊃an␈α⊂interpreter
␈↓ ↓H␈↓based on ␈↓αeval␈↓ has remained a feature of most LISP systems.

␈↓ ↓H␈↓        The␈αway␈α␈↓αeval␈↓␈αhandles␈αarguments␈αcorresponds␈αto␈αthe␈αcall-by-value␈αmethod␈αof␈αparameter␈αpassing
␈↓ ↓H␈↓in␈α∞ALGOL␈α∞and␈α∂similar␈α∞languages.␈α∞ There␈α∞is␈α∂also␈α∞a␈α∞form␈α∞of␈α∂␈↓αeval␈↓␈α∞that␈α∞corresponds␈α∂to␈α∞call-by-name.
␈↓ ↓H␈↓Here it is:

␈↓ ↓H␈↓        ␈↓αneval␈↓↓[␈↓αe, a␈↓↓] ← ␈↓βif at ␈↓αe␈↓β then
␈↓ ↓H␈↓β␈↓                ␈↓β␈↓↓[␈↓βif ␈↓αe ␈↓βeq ␈↓∧T ␈↓β then ␈↓∧T
␈↓ ↓H␈↓∧␈↓                ␈↓∧␈↓βelse if ␈↓αe ␈↓βeq ␈↓∧NIL ␈↓βthen ␈↓∧NIL
␈↓ ↓H␈↓∧␈↓                ␈↓∧␈↓βelse if ␈↓αnumberp e ␈↓βthen ␈↓αe
␈↓ ↓H␈↓α␈↓                ␈↓α␈↓βelse ␈↓αneval␈↓↓[␈↓βad ␈↓αassoc␈↓↓[␈↓αe, a␈↓↓], ␈↓βdd ␈↓α assoc␈↓↓[␈↓αe, a␈↓↓]]]

␈↓ ↓H␈↓↓␈↓        ␈↓↓␈↓βelse if at a ␈↓αe ␈↓β then
␈↓ ↓H␈↓β␈↓                ␈↓β␈↓↓[␈↓βif a ␈↓αe ␈↓βeq ␈↓∧CAR ␈↓βthen a ␈↓αneval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe ␈↓βeq ␈↓∧CDR ␈↓βthen d ␈↓αneval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe ␈↓βeq ␈↓∧CONS ␈↓βthen ␈↓αneval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]  . neval[␈↓βadd ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe ␈↓βeq ␈↓∧ATOM ␈↓βthen at ␈↓αneval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe ␈↓βeq ␈↓∧EQ ␈↓βthen ␈↓αneval␈↓↓[␈↓βad ␈↓αe, a␈↓↓]  ␈↓βeq ␈↓αneval␈↓↓[␈↓βadd ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe ␈↓βeq ␈↓∧QUOTE ␈↓βthen ad ␈↓αe
␈↓ ↓H␈↓α␈↓                ␈↓α␈↓βelse if a ␈↓αe ␈↓βeq ␈↓∧COND ␈↓βthen ␈↓αnevcon␈↓↓[␈↓βd ␈↓αe, a␈↓↓]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse if a ␈↓αe ␈↓βeq ␈↓∧LIST ␈↓βthen ␈↓αmapcar␈↓↓[␈↓βd ␈↓αe ␈↓↓, λ␈↓αx␈↓↓: ␈↓αneval␈↓↓[␈↓αx, a␈↓↓]]
␈↓ ↓H␈↓↓␈↓                ␈↓↓␈↓βelse ␈↓αneval␈↓↓[␈↓βd ␈↓αassoc␈↓↓[␈↓βa ␈↓αe, a␈↓↓] . ␈↓βd ␈↓αe, a␈↓↓]]

␈↓ ↓H␈↓↓␈↓        ␈↓↓␈↓βelse if aa ␈↓αe ␈↓βeq ␈↓∧LAMBDA ␈↓βthen ␈↓αneval␈↓↓[␈↓βadda ␈↓αe, nprup␈↓↓[␈↓βada ␈↓αe, ␈↓βd ␈↓αe␈↓↓,  ␈↓αa␈↓↓]]

␈↓ ↓H␈↓↓␈↓        ␈↓↓␈↓βelse if aa ␈↓αe ␈↓βeq ␈↓∧LABEL ␈↓βthen ␈↓αneval␈↓↓[␈↓βadda ␈↓αe  . ␈↓βd ␈↓αe, ␈↓↓[␈↓βada ␈↓αe . ␈↓βa ␈↓αe␈↓↓] . ␈↓αa␈↓↓], ␈↓

␈↓ ↓H␈↓where the auxiliary function ␈↓αnevcon␈↓ is given by

␈↓ ↓H␈↓        ␈↓αnevcon␈↓↓[␈↓αu, a␈↓↓] ← ␈↓βif ␈↓αneval␈↓↓[␈↓βaa ␈↓αu, a␈↓↓] ␈↓βthen  ␈↓αneval␈↓↓[␈↓βada ␈↓αu, a␈↓↓] ␈↓βelse ␈↓αnevcon␈↓↓[␈↓βd ␈↓αu, a␈↓↓].␈↓
␈↓ ↓H␈↓and nprup is
␈↓ ↓H␈↓        ␈↓αnprup␈↓↓[␈↓αu, v␈↓↓] ← ␈↓βif n ␈↓αu ␈↓βthen ␈↓αa ␈↓βelse ␈↓↓[␈↓βa ␈↓αu  . ␈↓↓[␈↓βa ␈↓αv . a␈↓↓]] . ␈↓αprup␈↓↓[␈↓βd ␈↓αu, ␈↓βd ␈↓αu␈↓↓].␈↓
␈↓ ↓H␈↓␈↓ ¬{CHAPTER IV␈↓ i4


␈↓ ↓H␈↓        The␈α⊂difference␈α⊃between␈α⊂␈↓αeval␈↓␈α⊃and␈α⊂␈↓αneval␈↓␈α⊃is␈α⊂only␈α⊃in␈α⊂two␈α⊃terms.␈α⊂ ␈↓αeval␈↓␈α⊃evaluates␈α⊂a␈α⊃variable␈α⊂by
␈↓ ↓H␈↓looking␈αit␈αup␈α
on␈αthe␈αassociation␈αlist␈α
whereas␈α␈↓αneval␈↓␈αlooks␈α
it␈αup␈αon␈αthe␈α
association␈αlist␈αand␈αevaluates␈α
the
␈↓ ↓H␈↓result␈α
in␈α
the␈α
context␈α
in␈α
which␈α
it␈α
was␈α
put␈α
on␈α
the␈α
association␈α
list.␈α
 Correspondingly,␈α
when␈αa␈α
λ-expression
␈↓ ↓H␈↓is␈α∂encountered,␈α∂␈↓αeval␈↓␈α∂forms␈α∂a␈α∂new␈α∂association␈α∂list␈α∂by␈α∂pairing␈α∂the␈α∂values␈α∂of␈α∂the␈α∂arguments␈α⊂with␈α∂the
␈↓ ↓H␈↓variables␈αbound␈αby␈αthe␈αλ␈αand␈αputting␈αthe␈αnew␈αpairs␈αin␈αfront␈αof␈αthe␈αold␈αassociation␈αlist,␈αwhereas␈α
␈↓αneval␈↓
␈↓ ↓H␈↓pairs␈αthe␈αarguments␈αthemselves␈αwith␈αthe␈αvariables␈αand␈αputs␈αthem␈αon␈αthe␈αfront␈αof␈αthe␈αassociation␈αlist.
␈↓ ↓H␈↓The␈αfunction␈αneval␈αalso␈αsaves␈αthe␈αcurrent␈αassociation␈α
list␈αwith␈αeach␈αvariable␈αon␈αthe␈αassociation␈αlist,␈α
so
␈↓ ↓H␈↓that␈α
the␈α∞variables␈α
can␈α∞be␈α
evaluated␈α
in␈α∞the␈α
correct␈α∞context.␈α
 In␈α
most␈α∞cases␈α
both␈α∞give␈α
the␈α∞same␈α
result
␈↓ ↓H␈↓with␈α⊂the␈α⊂same␈α∂work,␈α⊂but␈α⊂␈↓αneval␈↓␈α⊂gives␈α∂a␈α⊂result␈α⊂in␈α∂some␈α⊂cases␈α⊂in␈α⊂which␈α∂␈↓αeval␈↓␈α⊂loops.␈α⊂ An␈α⊂example␈α∂is
␈↓ ↓H␈↓obtained by evaluating ␈↓αF␈↓↓[2, 1]␈↓ where ␈↓αF␈↓ is defined by

␈↓ ↓H␈↓        ␈↓αF␈↓↓[␈↓αx, y␈↓↓] ← ␈↓βif␈↓α x␈↓↓=0 ␈↓βthen ␈↓↓0 ␈↓βelse ␈↓αF␈↓↓[␈↓αx␈↓↓-1, ␈↓αF␈↓↓[␈↓αy␈↓↓-2, ␈↓αx␈↓↓]].␈↓

␈↓ ↓H␈↓Exercises

␈↓ ↓H␈↓        1.␈α∞Write␈α∂␈↓αneval␈↓␈α∞and␈α∞the␈α∂necessary␈α∞auxiliary␈α∂functions␈α∞in␈α∞list␈α∂form,␈α∞and␈α∞try␈α∂them␈α∞out␈α∂on␈α∞some
␈↓ ↓H␈↓examples.



␈↓ ↓H␈↓2.

␈↓ ↓H␈↓3

␈↓ ↓H␈↓4␈↓βComputability.␈↓


␈↓ ↓H␈↓        Some␈α⊃LISP␈α⊃calculations␈α⊃run␈α⊃on␈α⊃indefinitely.␈α⊃ The␈α⊃most␈α⊃trivial␈α⊃case␈α⊃occurs␈α⊃if␈α⊃we␈α∩make␈α⊃the
␈↓ ↓H␈↓recursive definition

␈↓ ↓H␈↓        ␈↓αloop x ␈↓↓← ␈↓αloop x␈↓

␈↓ ↓H␈↓and␈αattempt␈αto␈α
compute␈α␈↓αloop␈↓↓[␈↓αx␈↓↓]␈↓␈αfor␈αany␈α
␈↓αx␈↓␈αwhatsoever.␈α Don't␈αdismiss␈α
this␈αexample␈αjust␈αbecause␈α
no-one
␈↓ ↓H␈↓would␈αwrite␈αsuch␈αan␈αobviously␈αuseless␈αfunction␈αdefinition.␈α There␈αis␈αa␈αsense␈αin␈αwhich␈αit␈αis␈αthe␈α"zero"
␈↓ ↓H␈↓of␈α
a␈α
large␈α
class␈αof␈α
non¬terminating␈α
function␈α
definitions,␈α
and,␈αas␈α
the␈α
Romans␈α
experienced␈α
but␈αnever
␈↓ ↓H␈↓learned, leaving zero out of the number system is a mistake.

␈↓ ↓H␈↓        Nevertheless,␈α⊂in␈α∂most␈α⊂programming,␈α∂non-terminating␈α⊂calculations␈α∂are␈α⊂the␈α∂results␈α⊂of␈α⊂errors␈α∂in
␈↓ ↓H␈↓defining␈α
functions.␈α
 Therefore,␈α
it␈α
would␈α
be␈α
useful␈α
to␈α
be␈α
able␈α
to␈α
tell␈α
whether␈α
a␈α
function␈αdefinition␈α
gives
␈↓ ↓H␈↓a␈α⊂result␈α⊂for␈α⊂all␈α∂arguments.␈α⊂ In␈α⊂fact,␈α⊂it␈α⊂would␈α∂be␈α⊂useful␈α⊂to␈α⊂be␈α⊂able␈α∂to␈α⊂tell␈α⊂whether␈α⊂a␈α⊂function␈α∂will
␈↓ ↓H␈↓terminate for a single argument.  Let us make this goal more precise.

␈↓ ↓H␈↓        Suppose␈α
that␈α
␈↓αf␈↓␈α
is␈α
a␈α
LISP␈α
function␈α
and␈α
␈↓αa␈↓␈α
is␈α
an␈α
S-expression,␈α
and␈α
we␈α
would␈α
like␈α
to␈αknow␈α
whether
␈↓ ↓H␈↓the␈α
computation␈α
of␈α
␈↓αf␈↓↓[␈↓αa␈↓↓]␈↓␈α
terminates.␈α
 Suppose␈α
␈↓αf␈↓␈α
is␈αrepresented␈α
by␈α
the␈α
S-expression␈α
␈↓αf*␈↓␈α
in␈α
the␈α
usual␈αS-
␈↓ ↓H␈↓expression␈α⊃notation␈α⊃for␈α⊃LISP␈α⊃functions.␈α⊃ Then␈α⊃the␈α⊃S-expression␈α⊃␈↓∧(f*␈α⊃(QUOTE␈α⊃a))␈↓␈α∩represents␈α⊃␈↓αf␈↓↓[␈↓αa␈↓↓]␈↓.
␈↓ ↓H␈↓Define␈α∂the␈α∞function␈α∂␈↓αterm␈↓␈α∞by␈α∂giving␈α∞␈↓αterm␈↓↓[␈↓αe␈↓↓]␈↓␈α∂the␈α∂value␈α∞␈↓βtrue␈↓α␈α∂if␈α∞e␈↓␈α∂is␈α∞an␈α∂S-expression␈α∞of␈α∂the␈α∂form␈α∞␈↓∧(f*
␈↓ ↓H␈↓␈↓ ¬{CHAPTER IV␈↓ i5


␈↓ ↓H␈↓∧(QUOTE␈α∂a))␈↓␈α∞for␈α∂which␈α∂␈↓αf␈↓↓[␈↓αa␈↓↓]␈↓␈α∞terminates␈α∂and␈α∂␈↓βfalse␈↓␈α∞otherwise.␈α∂ We␈α∞now␈α∂ask␈α∂whether␈α∞␈↓αterm␈↓␈α∂is␈α∂a␈α∞LISP
␈↓ ↓H␈↓function,␈α∞i.e.␈α
can␈α∞it␈α∞be␈α
constructed␈α∞from␈α
␈↓αcar,␈α∞cdr,␈α∞cons,␈α
atom,␈α∞␈↓␈α
and␈α∞␈↓αeq␈↓␈α∞using␈α
λ,␈α∞␈↓βlabel␈↓,␈α∞and␈α
conditional
␈↓ ↓H␈↓expressions?␈α
 Well,␈αit␈α
can't,␈αas␈α
we␈α
shall␈αshortly␈α
prove,␈αand␈α
this␈α
means␈αthat␈α
it␈αis␈α
not␈α␈↓αcomputable␈↓␈α
whether
␈↓ ↓H␈↓a␈α
LISP␈α
calculation␈α
terminates,␈α
since␈α
if␈α
␈↓αterm␈↓␈α
were␈α
computable␈α
by␈α
any␈α
computer␈α
or␈α
in␈α
any␈α
recognized
␈↓ ↓H␈↓sense, it could be represented as a LISP function.  Here is the proof:

␈↓ ↓H␈↓        Consider the function ␈↓αterma␈↓ defined from ␈↓αterm␈↓ by

␈↓ ↓H␈↓        ␈↓αterma u ␈↓↓← ␈↓βif␈↓α term list␈↓↓[␈↓αu, list␈↓↓[␈↓∧QUOTE␈↓α, u␈↓↓]] ␈↓βthen␈↓α loop u  ␈↓βelse true␈↓,

␈↓ ↓H␈↓and␈αsuppose␈αthat␈α␈↓αf␈↓␈αis␈α
a␈αLISP␈αfunction␈αand␈αthat␈α␈↓αf*␈↓␈α
is␈αits␈αS-expression␈αrepresentation.␈α What␈α
is␈α␈↓αterma
␈↓ ↓H␈↓αf*␈↓?␈α
 Well␈α
␈↓αterma␈α
f*␈↓␈α
tells␈α
us␈αwhether␈α
the␈α
computation␈α
of␈α
␈↓αf␈↓↓[␈↓αf*␈↓↓]␈↓␈α
terminates,␈αand␈α
it␈α
tells␈α
us␈α
this␈α
by␈αgoing
␈↓ ↓H␈↓into␈α∞a␈α
loop␈α∞if␈α
␈↓αf␈↓↓[␈↓αf*␈↓↓]␈↓␈α∞terminates␈α∞and␈α
giving␈α∞␈↓βtrue␈↓␈α
otherwise.␈α∞ Now␈α∞if␈α
␈↓αterm␈↓␈α∞were␈α
a␈α∞LISP␈α∞function,␈α
then
␈↓ ↓H␈↓␈↓αterma␈↓␈α∞would␈α∂also␈α∞be␈α∂a␈α∞LISP␈α∞function.␈α∂ Indeed␈α∞if␈α∂␈↓αterm␈↓␈α∞were␈α∞represented␈α∂by␈α∞the␈α∂S-expression␈α∞␈↓αterm*␈↓,
␈↓ ↓H␈↓then ␈↓αterma␈↓ would be represented by the S-expression

␈↓ ↓H␈↓        ␈↓αterma*␈α
␈↓∧=␈α(LAMBDA␈α
(U)␈α
(COND␈α((␈↓αterm*␈↓∧␈α
(LIST␈α
U␈α(LIST␈α
(QUOTE␈α
QUOTE)␈αU)))␈α
(LOOP␈α
U))␈α(T
␈↓ ↓H␈↓∧T))).

␈↓ ↓H␈↓∧Now␈α⊗consider␈α∃␈↓αterma␈↓↓[␈↓αterma*␈↓↓]␈↓.␈α⊗ According␈α⊗to␈α∃the␈α⊗definition␈α∃of␈α⊗␈↓αterma␈↓,␈α⊗this␈α∃will␈α⊗tell␈α⊗us␈α∃whether
␈↓ ↓H␈↓␈↓αterma␈↓↓[␈↓αterma*␈↓↓]␈↓␈αis␈αdefined,␈αi.e.␈αit␈αtells␈αabout␈αitself.␈α
 However,␈αit␈αgives␈αthis␈αanswer␈αin␈αa␈αcontradictory␈α
way;
␈↓ ↓H␈↓namely␈α␈↓αterma␈↓↓[␈↓αterma*␈↓↓]␈↓␈αlooping␈αtells␈αus␈αthat␈α␈↓αterma␈↓↓[␈↓αterma*␈↓↓]␈↓␈αterminates,␈αand␈α␈↓αterma␈↓↓[␈↓αterma*␈↓↓]␈↓␈αbeing␈α␈↓βtrue␈↓␈α
tells
␈↓ ↓H␈↓us␈αthat␈α␈↓αterma␈↓↓[␈↓αterma*␈↓↓]␈↓␈αdoesn't␈αterminate.␈α This␈αcontradiction␈αtells␈αus␈αthat␈α␈↓αterm␈↓␈αis␈αnot␈αa␈αLISP␈αfunction,
␈↓ ↓H␈↓and there is no general procedure for telling whether a LISP calculation terminates.

␈↓ ↓H␈↓        The␈α
above␈α
result␈α
does␈α
not␈α
exclude␈α
LISP␈α
functions␈α
that␈α
tell␈α
whether␈α
LISP␈αcalculations␈α
terminate.
␈↓ ↓H␈↓It␈α
just␈α
excludes␈α
perfect␈α
ones.␈α
 Suppose␈α
we␈α
have␈α
a␈α
function␈α
␈↓αt␈↓␈α
that␈α
sometimes␈α
says␈αcalculations␈α
terminate,
␈↓ ↓H␈↓sometimes␈α∞says␈α∂they␈α∞don't␈α∞terminate,␈α∂and␈α∞sometimes␈α∂runs␈α∞on␈α∞indefinitely.␈α∂ We␈α∞shall␈α∂further␈α∞assume
␈↓ ↓H␈↓that␈αwhen␈α
␈↓αt␈↓␈αgives␈α
an␈αanswer␈α
it␈αis␈α
always␈αright.␈α
 Given␈αsuch␈α
a␈αfunction␈α
we␈αcan␈α
improve␈αit␈α
a␈αbit␈αso␈α
that
␈↓ ↓H␈↓it␈α
will␈α
always␈α
give␈α
the␈αright␈α
answer␈α
when␈α
the␈α
calculation␈α
it␈αis␈α
asked␈α
about␈α
terminates.␈α
 This␈α
is␈αdone␈α
by
␈↓ ↓H␈↓mixing␈αthe␈αcomputation␈αof␈α␈↓αt␈↓↓[␈↓αe␈↓↓]␈↓␈αwith␈αa␈αcomputation␈αof␈α␈↓αeval␈↓↓[␈↓αe,␈α␈↓∧NIL␈↓↓]␈↓␈αdoing␈αthe␈αcomputations␈αalternately.
␈↓ ↓H␈↓If the ␈↓αeval␈↓↓[␈↓αe, ␈↓∧NIL␈↓↓]␈↓ computation ever terminates, then the new function asserts termination.

␈↓ ↓H␈↓        Given␈α
such␈α
a␈α␈↓αt␈↓,␈α
we␈α
can␈α
always␈αfind␈α
a␈α
calculation␈αthat␈α
does␈α
not␈α
terminate␈αbut␈α
␈↓αt␈↓␈α
doesn't␈α
say␈αso.
␈↓ ↓H␈↓The construction is just like that used in the previous proof.  Given ␈↓αt␈↓, we construct

␈↓ ↓H␈↓        ␈↓αta u ␈↓↓← ␈↓βif␈↓α t list␈↓↓[␈↓αu, list␈↓↓[␈↓∧QUOTE␈↓α, u␈↓↓]] ␈↓βthen␈↓α loop u  ␈↓βelse true␈↓,

␈↓ ↓H␈↓and␈α∞then␈α
we␈α∞consider␈α
␈↓αta␈↓↓[␈↓αta*␈↓↓]␈↓.␈α∞ If␈α
this␈α∞had␈α
the␈α∞value␈α
␈↓βtrue␈↓,␈α∞then␈α
it␈α∞wouldn't␈α
terminate␈α∞so␈α∞therefore␈α
it
␈↓ ↓H␈↓doesn't␈α
terminate␈α
but␈α
is␈α
not␈α
one␈α
of␈α
those␈α
expressions␈α
which␈α
␈↓αt␈↓␈α
decides.␈α
 Thus␈α
for␈α
any␈α
partial␈αdecider␈α
we
␈↓ ↓H␈↓can find a LISP calculation which doesn't terminate but which the decider doesn't decide.

␈↓ ↓H␈↓        This can in turn be used to get a slightly better decider, namely

␈↓ ↓H␈↓        ␈↓αt␈↓¬1␈↓↓[␈↓αe␈↓↓] ← ␈↓βif␈↓α e ␈↓↓= ␈↓αta* ␈↓βthen ␈↓∧DOESN'T-TERMINATE  ␈↓βelse␈↓α t␈↓↓[␈↓αe␈↓↓]␈↓.
␈↓ ↓H␈↓␈↓ ¬{CHAPTER IV␈↓ i6


␈↓ ↓H␈↓Of␈α
course,␈α
␈↓αt␈↓¬1␈↓␈αisn't␈α
much␈α
better␈α
than␈α␈↓αt␈↓,␈α
since␈α
it␈α
can␈αdecide␈α
only␈α
one␈α
more␈αcomputation,␈α
but␈α
we␈αcan␈α
form
␈↓ ↓H␈↓␈↓αt␈↓¬2␈↓␈α∞by␈α
applying␈α∞the␈α
same␈α∞process,␈α
and␈α∞so␈α
forth.␈α∞ In␈α
fact,␈α∞we␈α
can␈α∞even␈α
form␈α∞␈↓αt␈↓¬∞␈↓␈α
which␈α∞decides␈α∞all␈α
the
␈↓ ↓H␈↓cases␈αdecided␈αby␈α
any␈α␈↓αt␈↓¬n␈↓.␈α This␈αcan␈α
be␈αfurther␈αimproved␈αby␈α
the␈αsame␈αprocess,␈αetc.␈α
 How␈αfar␈αcan␈αwe␈α
go?
␈↓ ↓H␈↓The␈α
answer␈α∞is␈α
technical;␈α∞namely,␈α
the␈α∞improvement␈α
process␈α
can␈α∞be␈α
carried␈α∞out␈α
any␈α∞recursive␈α
ordinal
␈↓ ↓H␈↓number of times.

␈↓ ↓H␈↓        Unfortunately,␈α∪this␈α∀kind␈α∪of␈α∪improvement␈α∀seems␈α∪to␈α∀be␈α∪superficial,␈α∪since␈α∀none␈α∪of␈α∀the␈α∪new
␈↓ ↓H␈↓computations proved not to terminate are likely to be of practical interest.

␈↓ ↓H␈↓Exercises.

␈↓ ↓H␈↓1. Write a function that gives ␈↓αt␈↓¬n+1␈↓ in terms of ␈↓αt␈↓¬n␈↓.

␈↓ ↓H␈↓2. Write a function that gives ␈↓αt␈↓¬∞␈↓ in terms of ␈↓αt␈↓.

␈↓ ↓H␈↓3.␈α⊃If␈α⊃you␈α⊃know␈α⊃about␈α⊃Turing␈α⊃machines,␈α⊃write␈α⊃a␈α⊃LISP␈α⊃function␈α⊃to␈α⊃simulate␈α⊃an␈α⊃arbitrary␈α⊃Turing
␈↓ ↓H␈↓machine given a description of the machine in some convenient notation.

␈↓ ↓H␈↓4.␈αWrite␈αa␈αLISP␈αfunction␈αthat␈αwill␈αtranslate␈αa␈αTuring␈αmachine␈αdescription␈αinto␈αa␈αLISP␈αfunction␈αthat
␈↓ ↓H␈↓will do the same computation.

␈↓ ↓H␈↓5.␈α∂If␈α∂you␈α∞really␈α∂like␈α∂Turing␈α∞machines,␈α∂write␈α∂a␈α∞description␈α∂of␈α∂a␈α∞Turing␈α∂machine␈α∂that␈α∂will␈α∞interpret
␈↓ ↓H␈↓LISP internal notation.